Functional validation (verification) of complex IC designs is an activity that currently consumes a majority of the engineering man-hours for creating a design. The process of verification entails checking the output of a design implementation with that expected by some design reference model.
Verification of semiconductor chips can be done either through simulation or using formal methods. Simulation verification involves running a set of tests on the design and comparing the results of those tests with a reference model that produces the desired results.
A formal verification method is distinguished from simulation verification in that it uses mathematical models of the circuits to prove a property of interest rather than relying upon simulations of individual test cases. The advantage of a formal method is that, when it works, it is equivalent to doing an exhaustive simulation of every possible test case. Exhaustive simulation by itself is not practical for any but the most trivial of circuits because of the size of the state space.
Formal methods use a number of techniques to accomplish their mathematical proofs, including binary decision diagrams (BDDs), ordered BDDs, symbolic trajectory analysis (STA), satisfiability solvers (SAT), and bounded satisfiability solvers. The common thread in all these techniques is that they are algorithms for problems that, in computer science terms, are NP-complete. Without going into details, despite years of research, nobody has ever been able to solve an NP-complete problem with any algorithm whose worst-case run time does not grow exponentially in the size of the input. People therefore have to rely on heuristics to try to solve the problems in a reasonable time.
One important type of formal method is equivalence checking, which is used to verify that two circuits perform the same function. One of these circuits is considered to be the reference model specifying the ideal behavior of the circuit; the other circuit is a design model whose behavior is to be compared to the reference model. An example is comparing a register transfer level (RTL) circuit with the results of synthesizing it into a gate-level netlist. With equivalence checking, a design project could do most of its verification simulation cycles on the RTL design, which simulates more quickly, and then use equivalence checking to ensure that no bugs were introduced during synthesis.
For two circuits to be the same, each must have the same number of primary inputs (PIs) and the same number of primary outputs (POs), and there must be some way to identify corresponding inputs/outputs. Commercial combinational equivalence tools also require a complete correspondence between internal sequential elements (latches or flops) of the two designs. Based upon this matching, these tools convert the combinational circuit connecting any two corresponding pairs of state-holding elements into a canonical form like a binary decision diagram and compare for equality. If any pair of corresponding combinational circuits does not match, then the equivalence fails. By using correspondence points, the tools are able to keep the size of combinational circuits to be handled at any one time to a minimum, virtually eliminating capacity issues caused by the NP-completeness of the underlying problem.
Unfortunately, this view of equivalence is too restrictive to handle many transformations that are useful for optimizing speed or power. There are many modifications to a circuit that maintain the equality of computation at the PIs and POs while breaking the correspondence of circuits between sequential elements, such as:
1. Recoding of state machines
2. Retiming by moving logic across latch boundaries
3. Clock gating
4. Pipeline stage insertion/removal
5. Resource allocation
The generalized problem where matching of sequential elements cannot be assumed is referred to as sequential equivalence checking, which is an active area of research. The sequential equivalence checking problem space is much harder than that of combinational equivalence checking, so application of any algorithms for proving sequential equivalence may fail due to resource limitations.
When optimizing a design module, it is not necessary for the outputs to match in the case of invalid inputs. To address this issue, commercial sequential equivalence tools allow sets of input constraints to be specified. Ideally, the input constraints specify exactly the legal input space for the design to be verified. Unfortunately, the constraints themselves are subject to human error and require verification. If an overly restricted set of constraints is specified, then two designs may compare as equivalent even though they may have different outputs for legal inputs that were incorrectly excluded by the input constraints.
Likewise, it is not necessary for an output of a optimized design module to match the reference model during any time period when the output is not valid. For example, the data lines coming out of a memory module only have to match when a read operation on the memory causes the data to be read. To allow checking to be suppressed during times when an output is not valid, commercial sequential equivalence checking tools allow circuitry that computes a valid mask to be specified so that checking is disabled when the valid mask does not have the value encoding Boolean TRUE.
To meet aggressive timing goals, it is often necessary to modify the boundaries of modules and/or change the signal timing on the inter-module boundaries. Some signals may also be re-encoded in the optimized design relative to the original design.
If it were possible to run equivalence checking on the top-level design, nothing else would be necessary. However, because of capacity issues with sequential equivalence checking tools, it is necessary to break up the design into smaller parts and use blackboxes. FIG. 1 illustrates how blackboxing works. Assume that module B has already been shown equivalent to its corresponding reference module and that module A instantiates module B with three inputs and two outputs. Then we do a formal equivalence check of A treating the inputs of B as if they were POs of A and the outputs of B as if they were PIs of A, with the analogous blackboxing taking place in the reference model against which the design is being proved equivalent. Global equivalence is achieved by verifying the equivalence over all the optimized design modules.
As mentioned above, in order for formal equivalence checking tools to work, the tools require the two modules to have identical PIs and POs. However, when decomposing equivalence checking hierarchically, there may be design modules that differ from the reference model due to changed boundaries, retimed ports, or encoded ports. All the information on how a module's boundary is redrawn, retimed, and encoded is contained in the module's configuration file which is an input to the disclosed invention.
This method reads a reference model, reads the configuration file for an optimized design module and creates a set of modified reference modules and a pair of wrappers such that the wrappers have the same PIs and POs with identical timing, but one encapsulates the reference model and the other the design module. If the two wrappers are proved equivalent, this proof guarantees that the design module faithfully implements the interface changes specified in its configuration file.
The configuration file for a design module contains the following information for each of the design module's ports:                1. A reference connection that specifies how to create the equivalent of the design module port based on some Boolean combination of signals within the reference model.        2. An encoding function, defaulting to the identity function, translating the reference connection to the design module port. An encoding function is a special case of a Boolean combination, specifically one for converting a multi-bit signal to a different representation. An example of an encoding function is to convert a binary encoding to a one-hot encoding. Encoding functions are a mere convenience and do not add any additional domain of applicability to the disclosed invention.        3. A delay value, in units of clock cycles, defaulting to 0, for how the timing of the design module port relates to that of the reference connection, in an embodiment of this invention that supports delays. Positive values mean that the design module port changes later than the reference connection and negative values that it changes earlier.        4. A valid mask that is a Boolean expression, defaulting to Boolean TRUE, possibly containing references to signals within the reference model, which specifies when the value of an output port is expected to match its reference expression, in an embodiment of the disclosed invention that supports valid masks.        
This application claims the benefits of the earlier filed U.S. Provisional Application Ser. No. 61/112,537, filed 7 Nov. 2008, which is incorporated by reference for all purposes into this specification.